\begin{tabbing}
$\forall$\=${\it es}$:ES, $k$:Knd, $l$:IdLnk, ${\it tg}$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $n$:$\mathbb{N}$, $a$:ecl(${\it ds}$;${\it da}$),\+
\\[0ex]$f$:(State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$${\it da}$(rcv($l$,${\it tg}$))?Void).
\-\\[0ex]es{-}decls(${\it es}$;source($l$);${\it ds}$;${\it da}$)
\\[0ex]$\Rightarrow$ (\=with decls \=${\it ds}$ \+\+
\\[0ex]${\it da}$
\-\\[0ex]sends on $l$ from $e$ 
\\[0ex]include \=if \=kind($e$) = $k$ $\wedge_{2}$ action[[$a$ $n$]][es{-}init(${\it es}$;$e$);$e$]$\rightarrow$\+\+
\\[0ex][$\langle$${\it tg}$$,\,$$f$((state when $e$),val($e$))$\rangle$]
\-\\[0ex]else nil fi 
\-\\[0ex]and only these for tags in [${\it tg}$]
\\[0ex]$\Leftrightarrow$
\\[0ex]es{-}sends{-}iff2(${\it es}$;$l$;${\it tg}$;${\it da}$(rcv($l$,${\it tg}$))?Top;${\it ds}$;$e$.kind($e$) $=$ $k$
\\[0ex]\& ecl{-}es{-}act(${\it es}$;$n$;$a$)(es{-}init(${\it es}$;$e$),$e$);$e$.$f$((state when $e$),val($e$))))
\-
\end{tabbing}